KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmpU1AUcg/vangelder_typed.xml









The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS


↳1 DecreasingLoopProof (⇔, 993 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 7 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

head(Cons(x, xs)) → x

e(Cons(F, Nil), b) → False

e(Cons(T, Nil), b) → False

e(Cons(B, Nil), b) → False

e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)

e(Cons(F, Cons(x, xs)), b) → False

e(Cons(T, Cons(x, xs)), b) → False

e(Cons(B, Cons(x, xs)), b) → False

e(Cons(A, Cons(x, xs)), b) → False

equal(F, F) → True

equal(F, T) → False

equal(F, B) → False

equal(F, A) → False

equal(T, F) → False

equal(T, T) → True

equal(T, B) → False

equal(T, A) → False

equal(B, F) → False

equal(B, T) → False

equal(B, B) → True

equal(B, A) → False

equal(A, F) → False

equal(A, T) → False

equal(A, B) → False

equal(A, A) → True

notEmpty(Cons(x, xs)) → True

notEmpty(Nil) → False

e(Nil, b) → False

t(x, y) → t[Ite](e(x, y), x, y)

r(x, y) → r[Ite](e(x, y), x, y)

q(x, y) → q[Ite](e(x, y), x, y)

p(x, y) → p[Ite](e(x, y), x, y)

goal(x, y) → q(x, y)

The (relative) TRS S consists of the following rules:

and(False, False) → False

and(True, False) → False

and(False, True) → False

and(True, True) → True

q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))

q[Ite](False, x, Cons(F, Cons(T, xs))) → False

q[Ite](False, x, Cons(F, Cons(B, xs))) → False

q[Ite](False, x, Cons(F, Cons(A, xs))) → False

q[Ite](False, x, Cons(T, Cons(F, xs))) → False

q[Ite](False, x, Cons(T, Cons(T, xs))) → False

q[Ite](False, x, Cons(T, Cons(B, xs))) → False

q[Ite](False, x, Cons(T, Cons(A, xs))) → False

q[Ite](False, x, Cons(B, Cons(F, xs))) → False

q[Ite](False, x, Cons(B, Cons(T, xs))) → False

q[Ite](False, x, Cons(B, Cons(B, xs))) → False

q[Ite](False, x, Cons(B, Cons(A, xs))) → False

q[Ite](False, x, Cons(A, Cons(F, xs))) → False

q[Ite](False, x, Cons(A, Cons(T, xs))) → False

q[Ite](False, x, Cons(A, Cons(B, xs))) → False

q[Ite](False, x, Cons(A, Cons(A, xs))) → False

q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))

q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))

q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))

q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))

r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))

r[Ite](False, x, Cons(T, xs)) → False

r[Ite](False, x, Cons(B, xs)) → False

r[Ite](False, x, Cons(A, xs)) → False

p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))

p[Ite](False, x, Cons(T, xs)) → False

p[Ite](False, x, Cons(B, xs)) → False

p[Ite](False, x, Cons(A, xs)) → False

q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))

t[Ite](False, x, y) → True

t[Ite](True, x, y) → True

r[Ite](True, x, y) → True

q[Ite](True, x, y) → True

q[Ite][False][Ite](False, x, y) → False

p[Ite](True, x, y) → True

Rewrite Strategy: INNERMOST




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
r(Cons(F, Nil), Cons(F, xs8693_0)) →+ r[Ite][False][Ite][True][Ite](and(q(Cons(F, Nil), xs8693_0), r(Cons(F, Nil), xs8693_0)), Cons(F, Nil), Cons(F, xs8693_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].
The pumping substitution is [xs8693_0 / Cons(F, xs8693_0)].
The result substitution is [ ].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

head(Cons(x, xs)) → x

e(Cons(F, Nil), b) → False

e(Cons(T, Nil), b) → False

e(Cons(B, Nil), b) → False

e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)

e(Cons(F, Cons(x, xs)), b) → False

e(Cons(T, Cons(x, xs)), b) → False

e(Cons(B, Cons(x, xs)), b) → False

e(Cons(A, Cons(x, xs)), b) → False

equal(F, F) → True

equal(F, T) → False

equal(F, B) → False

equal(F, A) → False

equal(T, F) → False

equal(T, T) → True

equal(T, B) → False

equal(T, A) → False

equal(B, F) → False

equal(B, T) → False

equal(B, B) → True

equal(B, A) → False

equal(A, F) → False

equal(A, T) → False

equal(A, B) → False

equal(A, A) → True

notEmpty(Cons(x, xs)) → True

notEmpty(Nil) → False

e(Nil, b) → False

t(x, y) → t[Ite](e(x, y), x, y)

r(x, y) → r[Ite](e(x, y), x, y)

q(x, y) → q[Ite](e(x, y), x, y)

p(x, y) → p[Ite](e(x, y), x, y)

goal(x, y) → q(x, y)

The (relative) TRS S consists of the following rules:

and(False, False) → False

and(True, False) → False

and(False, True) → False

and(True, True) → True

q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))

q[Ite](False, x, Cons(F, Cons(T, xs))) → False

q[Ite](False, x, Cons(F, Cons(B, xs))) → False

q[Ite](False, x, Cons(F, Cons(A, xs))) → False

q[Ite](False, x, Cons(T, Cons(F, xs))) → False

q[Ite](False, x, Cons(T, Cons(T, xs))) → False

q[Ite](False, x, Cons(T, Cons(B, xs))) → False

q[Ite](False, x, Cons(T, Cons(A, xs))) → False

q[Ite](False, x, Cons(B, Cons(F, xs))) → False

q[Ite](False, x, Cons(B, Cons(T, xs))) → False

q[Ite](False, x, Cons(B, Cons(B, xs))) → False

q[Ite](False, x, Cons(B, Cons(A, xs))) → False

q[Ite](False, x, Cons(A, Cons(F, xs))) → False

q[Ite](False, x, Cons(A, Cons(T, xs))) → False

q[Ite](False, x, Cons(A, Cons(B, xs))) → False

q[Ite](False, x, Cons(A, Cons(A, xs))) → False

q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))

q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))

q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))

q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))

r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))

r[Ite](False, x, Cons(T, xs)) → False

r[Ite](False, x, Cons(B, xs)) → False

r[Ite](False, x, Cons(A, xs)) → False

p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))

p[Ite](False, x, Cons(T, xs)) → False

p[Ite](False, x, Cons(B, xs)) → False

p[Ite](False, x, Cons(A, xs)) → False

q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))

t[Ite](False, x, y) → True

t[Ite](True, x, y) → True

r[Ite](True, x, y) → True

q[Ite](True, x, y) → True

q[Ite][False][Ite](False, x, y) → False

p[Ite](True, x, y) → True

Rewrite Strategy: INNERMOST




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
Innermost TRS:
Rules:
head(Cons(x, xs)) → x
e(Cons(F, Nil), b) → False
e(Cons(T, Nil), b) → False
e(Cons(B, Nil), b) → False
e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)
e(Cons(F, Cons(x, xs)), b) → False
e(Cons(T, Cons(x, xs)), b) → False
e(Cons(B, Cons(x, xs)), b) → False
e(Cons(A, Cons(x, xs)), b) → False
equal(F, F) → True
equal(F, T) → False
equal(F, B) → False
equal(F, A) → False
equal(T, F) → False
equal(T, T) → True
equal(T, B) → False
equal(T, A) → False
equal(B, F) → False
equal(B, T) → False
equal(B, B) → True
equal(B, A) → False
equal(A, F) → False
equal(A, T) → False
equal(A, B) → False
equal(A, A) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
e(Nil, b) → False
t(x, y) → t[Ite](e(x, y), x, y)
r(x, y) → r[Ite](e(x, y), x, y)
q(x, y) → q[Ite](e(x, y), x, y)
p(x, y) → p[Ite](e(x, y), x, y)
goal(x, y) → q(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
q[Ite](False, x, Cons(F, Cons(T, xs))) → False
q[Ite](False, x, Cons(F, Cons(B, xs))) → False
q[Ite](False, x, Cons(F, Cons(A, xs))) → False
q[Ite](False, x, Cons(T, Cons(F, xs))) → False
q[Ite](False, x, Cons(T, Cons(T, xs))) → False
q[Ite](False, x, Cons(T, Cons(B, xs))) → False
q[Ite](False, x, Cons(T, Cons(A, xs))) → False
q[Ite](False, x, Cons(B, Cons(F, xs))) → False
q[Ite](False, x, Cons(B, Cons(T, xs))) → False
q[Ite](False, x, Cons(B, Cons(B, xs))) → False
q[Ite](False, x, Cons(B, Cons(A, xs))) → False
q[Ite](False, x, Cons(A, Cons(F, xs))) → False
q[Ite](False, x, Cons(A, Cons(T, xs))) → False
q[Ite](False, x, Cons(A, Cons(B, xs))) → False
q[Ite](False, x, Cons(A, Cons(A, xs))) → False
q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
r[Ite](False, x, Cons(T, xs)) → False
r[Ite](False, x, Cons(B, xs)) → False
r[Ite](False, x, Cons(A, xs)) → False
p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))
p[Ite](False, x, Cons(T, xs)) → False
p[Ite](False, x, Cons(B, xs)) → False
p[Ite](False, x, Cons(A, xs)) → False
q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
t[Ite](False, x, y) → True
t[Ite](True, x, y) → True
r[Ite](True, x, y) → True
q[Ite](True, x, y) → True
q[Ite][False][Ite](False, x, y) → False
p[Ite](True, x, y) → True

Types:
head :: Cons:Nil → F:T:B:A
Cons :: F:T:B:A → Cons:Nil → Cons:Nil
e :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
F :: F:T:B:A
Nil :: Cons:Nil
False :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
T :: F:T:B:A
B :: F:T:B:A
A :: F:T:B:A
e[Match][Cons][Ite][True][Match] :: F:T:B:A → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
equal :: F:T:B:A → F:T:B:A → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
True :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
notEmpty :: Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
t :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
t[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
p :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
p[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
goal :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
and :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite][False][Ite][True][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite][False][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r[Ite][False][Ite][True][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
hole_F:T:B:A1_0 :: F:T:B:A
hole_Cons:Nil2_0 :: Cons:Nil
hole_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]3_0 :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]5_0 :: Nat → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
r, q, p
They will be analysed ascendingly in the following order:
r = q
r = p
q = p




(8) Obligation:
Innermost TRS:
Rules:
head(Cons(x, xs)) → x
e(Cons(F, Nil), b) → False
e(Cons(T, Nil), b) → False
e(Cons(B, Nil), b) → False
e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)
e(Cons(F, Cons(x, xs)), b) → False
e(Cons(T, Cons(x, xs)), b) → False
e(Cons(B, Cons(x, xs)), b) → False
e(Cons(A, Cons(x, xs)), b) → False
equal(F, F) → True
equal(F, T) → False
equal(F, B) → False
equal(F, A) → False
equal(T, F) → False
equal(T, T) → True
equal(T, B) → False
equal(T, A) → False
equal(B, F) → False
equal(B, T) → False
equal(B, B) → True
equal(B, A) → False
equal(A, F) → False
equal(A, T) → False
equal(A, B) → False
equal(A, A) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
e(Nil, b) → False
t(x, y) → t[Ite](e(x, y), x, y)
r(x, y) → r[Ite](e(x, y), x, y)
q(x, y) → q[Ite](e(x, y), x, y)
p(x, y) → p[Ite](e(x, y), x, y)
goal(x, y) → q(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
q[Ite](False, x, Cons(F, Cons(T, xs))) → False
q[Ite](False, x, Cons(F, Cons(B, xs))) → False
q[Ite](False, x, Cons(F, Cons(A, xs))) → False
q[Ite](False, x, Cons(T, Cons(F, xs))) → False
q[Ite](False, x, Cons(T, Cons(T, xs))) → False
q[Ite](False, x, Cons(T, Cons(B, xs))) → False
q[Ite](False, x, Cons(T, Cons(A, xs))) → False
q[Ite](False, x, Cons(B, Cons(F, xs))) → False
q[Ite](False, x, Cons(B, Cons(T, xs))) → False
q[Ite](False, x, Cons(B, Cons(B, xs))) → False
q[Ite](False, x, Cons(B, Cons(A, xs))) → False
q[Ite](False, x, Cons(A, Cons(F, xs))) → False
q[Ite](False, x, Cons(A, Cons(T, xs))) → False
q[Ite](False, x, Cons(A, Cons(B, xs))) → False
q[Ite](False, x, Cons(A, Cons(A, xs))) → False
q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
r[Ite](False, x, Cons(T, xs)) → False
r[Ite](False, x, Cons(B, xs)) → False
r[Ite](False, x, Cons(A, xs)) → False
p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))
p[Ite](False, x, Cons(T, xs)) → False
p[Ite](False, x, Cons(B, xs)) → False
p[Ite](False, x, Cons(A, xs)) → False
q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
t[Ite](False, x, y) → True
t[Ite](True, x, y) → True
r[Ite](True, x, y) → True
q[Ite](True, x, y) → True
q[Ite][False][Ite](False, x, y) → False
p[Ite](True, x, y) → True

Types:
head :: Cons:Nil → F:T:B:A
Cons :: F:T:B:A → Cons:Nil → Cons:Nil
e :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
F :: F:T:B:A
Nil :: Cons:Nil
False :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
T :: F:T:B:A
B :: F:T:B:A
A :: F:T:B:A
e[Match][Cons][Ite][True][Match] :: F:T:B:A → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
equal :: F:T:B:A → F:T:B:A → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
True :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
notEmpty :: Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
t :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
t[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
p :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
p[Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
goal :: Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
and :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite][False][Ite][True][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
q[Ite][False][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
r[Ite][False][Ite][True][Ite] :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite] → Cons:Nil → Cons:Nil → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
hole_F:T:B:A1_0 :: F:T:B:A
hole_Cons:Nil2_0 :: Cons:Nil
hole_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]3_0 :: False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]5_0 :: Nat → False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]
Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(F, gen_Cons:Nil4_0(x))
gen_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]5_0(0) ⇔ False
gen_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]5_0(+(x, 1)) ⇔ q[Ite][False][Ite][True][Ite](gen_False:e[Match][Cons][Ite][True][Match]:True:q[Ite][False][Ite][True][Ite]:r[Ite][False][Ite][True][Ite]5_0(x), Nil, Nil)
The following defined symbols remain to be analysed:
q, r, p
They will be analysed ascendingly in the following order:
r = q
r = p
q = p